$\forall$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), ${\it rt}$:(Id$\rightarrow$Id), ${\it rtinv}$:(Id$\rightarrow$(Id+Unit)).
\\[0ex]inv{-}rel(Id;Id;${\it rt}$;${\it rtinv}$)
\\[0ex]$\Rightarrow$ ($\forall$$m$:Msg($M$). isl(${\it rtinv}$(mtag($m$))) $\Rightarrow$ msg{-}rename(${\it rtinv}$;$m$) $\in$ Msg($\lambda$$l$,${\it tg}$. $M$($l$,${\it rt}$(${\it tg}$))))